/*
 * $Id: ConsentBackend.java 1259 2007-01-09 14:23:47Z tcoupaye $
 *
 * Behavior Protocols extensions for static and runtime checking
 * developed for the Julia implementation of Fractal.
 *
 * Copyright 2004
 *    Distributed Systems Research Group
 *    Department of Software Engineering
 *    Faculty of Mathematics and Physics
 *    Charles University, Prague
 *
 * Copyright (C) 2006
 *    Formal Methods In Software Engineering Group
 *    Institute of Computer Science
 *    Academy of Sciences of the Czech Republic
 *
 * Copyright (C) 2006 France Telecom
 *
 * This library is free software; you can redistribute it and/or
 * modify it under the terms of the GNU Lesser General Public
 * License as published by the Free Software Foundation; either
 * version 2 of the License, or (at your option) any later version.
 *
 * This library is distributed in the hope that it will be useful,
 * but WITHOUT ANY WARRANTY; without even the implied warranty of
 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU
 * Lesser General Public License for more details.
 *
 * You should have received a copy of the GNU Lesser General Public
 * License along with this library; if not, write to the Free Software
 * Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA  02111-1307 USA
 *
 * Contact: ft@nenya.ms.mff.cuni.cz
 * Authors: Jan Kofron <kofron@nenya.ms.mff.cuni.cz>
 */

package org.objectweb.fractal.bpc.checker.backend;

import java.util.TreeSet;

import org.objectweb.fractal.bpc.checker.CheckingResult;
import org.objectweb.fractal.bpc.checker.DFSR.*;
import org.objectweb.fractal.bpc.checker.node.*;
import org.objectweb.fractal.bpc.checker.optimizer.OptExplicit;
import org.objectweb.fractal.bpc.checker.parser.Debug;
import org.objectweb.fractal.bpc.checker.state.Signature;
import org.objectweb.fractal.bpc.checker.state.TransitionPair;


/**
 * This class joins two preotocols via a consent operator and perform the
 * consensual compliance test.
 */
public class ConsentBackend implements IBackend {

    /**
     * Creates a new instance of ConsentBackend.
     * @param repository action repository
     */
    public ConsentBackend(ActionRepository repository) {
        this.repository = repository;
    }

    /**
     * Checks the consensual compliance and composition of protocols in the way that
     * it creates an "inverse" protocol of the frame protocol and then tries to
     * combine the protocols using consent operator.
     * 
     * @param nodes two or more parse tree nodes for two or more protocols are expected (architecture-frame and subcomponents-frame)
     * @param synchroops synchro operations for the consent operator for the sequence of protocols.
     * @param unboundops methods of unbound interfaces.
     *  
     */
    public CheckingResult perform(TreeNode[] nodes, String[] synchroops, String[] unboundops) {

        //basic checking of parameters
        if (nodes.length < 2) {
            return new CheckingResult(CheckingResult.ERR_OTHERERROR, "Consent backend: wrong number of items within the first array parameter (at least two required).\n");
        }

        if (synchroops.length != nodes.length - 1) {
            return new CheckingResult(CheckingResult.ERR_OTHERERROR, "Consent backend: wrong number of items within the second array parameter (1 lower than the number of components required).\n");
        }

        // invert the frame protocol, if it is a frame protocol, i.e. we are
        // testing compliance
        if (Options.action == Options.ACTIONTESTCOMPLIANCE)
            nodes[0] = invertProtocol(nodes[0], repository);

        TreeNode result = new DeterministicNode(nodes[nodes.length - 1]);

        TreeSet unbound = new TreeSet();
        for (int y = 0; y < unboundops.length; ++y) {
        	  try {
            	unbound.add(new Integer(repository.getItemIndex(unboundops[y])));
            }
            catch (NullPointerException e) {}
        }

        for (int j = nodes.length - 2; j > 0; --j) {
            String[] sprov;
            TreeSet prov = new TreeSet();
            sprov = synchroops[j].equals("") ? new String[0] : synchroops[j].split(",");

            for (int i = 0; i < sprov.length; ++i) {
                int index;
                try {
                    index = repository.getItemIndex(sprov[i]);
                }
                catch (NullPointerException e) {
                	  continue;
                    //return new CheckingResult(CheckingResult.ERR_OTHERERROR, "Invalid provisions '" + sprov[i] + "' - not occuring within the protocols.");
                } 

                prov.add(new Integer(index));
            }

            // create the consent node joining the two protocols
            result = new ConsentNode(new DeterministicNode(nodes[j]), result, prov, new TreeSet(), repository, true);
        }

        //-------------- consensual compliance test
        String[] sprov;
        TreeSet prov = new TreeSet();
        //sprov = synchroops[0].split(",");
        sprov = synchroops[0].equals("") ? new String[0] : synchroops[0].split(",");

        for (int i = 0; i < sprov.length; ++i) {
            int index;
            try {
                index = repository.getItemIndex(sprov[i]);
            }
            catch (NullPointerException e) {
                //return new CheckingResult(CheckingResult.ERR_OTHERERROR, "Invalid provisions '" + sprov[i] + "' - not occuring within the protocols.");
                continue;
            } 
            prov.add(new Integer(index));
        }

        ConsentNode top = new ConsentNode(new DeterministicNode(nodes[0]), result, prov, unbound, repository, true);
        
        Debug.println("State space estimate: " + top.getWeight());

        // perform the forward cutting and explicit optimizations
        Debug.print("Optimizing the parse tree for the composition test......");

        try {
            if (Options.forwardcutting)
                top = (ConsentNode) top.forwardCut(repository.getAllUsedEventIndices());
            
            if (top != null)
                Signature.setSize(top.getLeafCount());

            if ((Options.explicit) && (top != null))
                top = (ConsentNode) new OptExplicit(top, Options.explicitsize).perform();
        } catch (InvalidParameterException e) {
            return new CheckingResult(CheckingResult.ERR_OTHERERROR, "Error while performing optimization. Bailing out....");
        }

        Debug.println("done.");
        /**/

        // check the compliance
        if (top != null) {
            
            TransitionPair.repository = repository;
            
            DFSRTraverser dfsr1 = new DFSRTraverser(top, repository);

            try {
                dfsr1.run(new DFSRConsent(top));
            } catch (AcceptingStateException e) {
                return new CheckingResult(CheckingResult.ERR_OTHERERROR, "Internal Checker error " + e.getMessage());
            } catch (BadActivityException e) {
                return new CheckingResult(CheckingResult.ERR_BADACTIVITY, "Composition error detected - " + e.getMessage());
            } catch (NoActivityException e) {
                return new CheckingResult(CheckingResult.ERR_NOACTIVITY, "Composition error detected - " + e.getMessage());
            } catch (InfiniteActivityException e) {
                return new CheckingResult(CheckingResult.ERR_INFINITEACTIVITY, "Composition error detected - " + e.getMessage());
            } catch (CheckingException e) {
                return new CheckingResult(CheckingResult.ERR_OTHERERROR, "Unknown error while checking - " + e.getMessage());
            } catch (InvalidParameterException e) {
                return new CheckingResult(CheckingResult.ERR_OTHERERROR, "Error while checking (Invalid parameter exception): " + e.getMessage());
            } catch (ItemAlreadyPresentException e) {
                return new CheckingResult(CheckingResult.ERR_OTHERERROR, "Error while checking (ItemAlreadyPresentException): " + e.getMessage());
            } catch (ItemNotPresentException e) {
                return new CheckingResult(CheckingResult.ERR_OTHERERROR, "Error while checking (ItemNotPresentException): " + e.getMessage());
            }
        } else
            Debug.println("Warning: Automaton for consent is empty!");

        Debug.println("Protocols are composition error free.");

        return new CheckingResult(CheckingResult.ERR_OK, "OK");
    }

    public static TreeNode invertProtocol(TreeNode protocol, ActionRepository repository) {

        if (protocol instanceof EventNode) {
            return new EventNode(repository.getInverseAction(((EventNode) protocol).getEventIndex()), repository);
        }
        else if (protocol instanceof AtomicNode) {
            return new AtomicNode(repository.getInverseAction(((AtomicNode) protocol).getEventIndex()), repository);
        }
        else if ((protocol instanceof AlternativeNode) && (((AlternativeNode)protocol).getorparallel())) {
            protocol.changeChild(2, invertProtocol(protocol.getChildren()[2], repository));
            
            if (protocol.getChildren()[0] instanceof EventNode)
                protocol.changeChild(0, invertProtocol(protocol.getChildren()[0], repository));
                
            if (protocol.getChildren()[1] instanceof EventNode)
                protocol.changeChild(1, invertProtocol(protocol.getChildren()[1], repository));
            
            return protocol;
        
        } else {
            TreeNode[] children = protocol.getChildren();
            for (int i = 0; i < children.length; ++i) {
                protocol.changeChild(i, invertProtocol(children[i], repository));
            }

            return protocol;
        }
    }
    
    
    //-----------------------------------------------------------------

    /**
     * Action repository for protocol inversion
     */
    private ActionRepository repository;

}
